Nuprl Lemma : decidable__l_all
4,23
postcript
pdf
A
:Type,
F
:(
A
Prop),
L
:
A
List. (
k
:
A
. Dec(
F
(
k
)))
Dec(
k
L
.
F
(
k
))
latex
Definitions
t
T
,
Prop
,
x
(
s
)
,
x
:
A
.
B
(
x
)
,
Dec(
P
)
,
x
L
.
P
(
x
)
,
P
Q
,
x
.
t
(
x
)
,
A
,
P
Q
,
P
&
Q
,
P
Q
,
P
Q
Lemmas
decidable
cand
,
decidable
functionality
,
l
all
cons
,
not
wf
,
l
all
wf
,
l
all
nil
,
decidable
wf
origin
A:Type, F:(A
Prop), L:A List. (k:A. Dec(F(k))) 
Dec(k
L. F(k)) A:Type, F:(AProp), L:A List. (k:A. Dec(F(k))) Dec(kL. F(k)) Tx:A. B(x)xL. P(x) Q
x. t(x)
A
Q
Q Q